CLASS BSTree [Element:WithOrder]
IS-SUBTYPE-OF BTree[Element]
BASIC CONSTRUCTORS  BSTree_Insert
EFFECTIVE
OPERATIONS
  BSTree_Insert: BSTree(t) * Element(e) -> BSTree
      pre: not belongs(e, t);
  BSTree_Delete: BSTree(t) * Element(e) -> BSTree
      pre: not BTree_IsEmpty(t);
  BSTree_Min: BSTree(t) -> Element
      pre: not BTree_IsEmpty(t);
AXIOMS  b1, b2: BSTree;    i, j: Element;
  BSTree_Insert(BTree_Empty() as BSTree, i) =
      BTree_Create(BTree_Empty() as BSTree, BTree_Empty() as BSTree, i) as BSTree;
  (i < j) implies
  BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
      BTree_Create(BSTree_Insert(b1, i), b2, j) as BSTree;
  (i > j) implies
  BSTree_Insert(BTree_Create(b1, b2, j) as BSTree, i) =
      BTree_Create(b1, BSTree_Insert(b2, i), j) as BSTree;
  BTree_IsEmpty(b1) implies
  BSTree_Min(BTree_Create(b1, b2, i) as BSTree) = i;
  not BTree_IsEmpty(b1) implies
  BSTree_Min(BTree_Create(b1, b2, i) as BSTree) =
      BSTree_Min(b1);
  (j < i) implies
  BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
      BTree_Create(BSTree_Delete(b1, j), b2, i) as BSTree;
  (j > i) implies
  BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
      BTree_Create(b1, BSTree_Delete(b2, j), i) as BSTree;
  (j = i and BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
      BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
          BTree_Empty() as BSTree;
  (j = i and BTree_IsEmpty(b1) and not BTree_IsEmpty(b2)) implies
      BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
          b2;
  (j = i and not BTree_IsEmpty(b1) and BTree_IsEmpty(b2)) implies
      BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
          b1;
  (j = i and not BTree_IsEmpty(b1) and not BTree_IsEmpty(b2)) implies
      BSTree_Delete(BTree_Create(b1, b2, i) as BSTree, j) =
          BTree_Create(
              b1,
              BSTree_Delete(b2, BSTree_Min(b2)),
              BSTree_Min(b2)
          ) as BSTree;
END-CLASS
